



To our knowledge, ours is the first attempt to incorporate adaptation (or evolvability) constructs  into 
a session process language. 
Related to our work are efforts 
on formal models for service-oriented systems
with constructs such as exceptions and compensations (e.g.,~\cite{DBLP:conf/concur/CarboneHY08,DBLP:books/sp/sensoria2011/FerreiraLRVZ11}). 
In particular,~\cite{DBLP:conf/concur/CarboneHY08} develops a typeful approach for \emph{interactional exceptions}
in asynchronous session types. There, services define a default process and an exception handler, and may be influenced by 
a $\mathtt{throw}$ construct used to throw exceptions;
the goal of the typing system is to ensure consistent dynamic escaping from possibly nested exception scopes in a concerted way.

Notions 
such as exceptions and compensations are conceptually different from our intended notion of runtime adaptation.
In fact, in our view, such notions 
represent only a particular instance of adaptation/evolvabilty scenarios. 
This way, forms of exceptions (e.g., the one in~\cite{DBLP:conf/concur/CarboneHY08}) should typically handle \emph{internal events}
which  arise during the program's execution and may affect its flow of control. 
Similar in several respects to exceptions, mechanisms for compensations are usually conceived for 
handling events which are often exceptional \emph{and} catastrophic, such as runtime errors.
In contrast, runtime adaptation in modern distributed systems 
relies on \emph{external} mechanisms tailored to 
handle more general events, not necessarily catastrophic.
A familiar example of such events are program upgrades, whose execution can be anticipated and incorporated into the program's code for eventual execution. 
As another  example, consider elasticity in cloud-based applications, 
i.e., the ability such applications have to acquire/release computing resources based on user demand.
%depending on user activity, they determine how/when to .
%that in peaks of high activity additional computing resources must be acquired.
Although elasticity triggers 
%Such peaks, while triggering 
system adaptation, % of the system architecture, 
it does not represent a catastrophic event; rather, 
it represents an acceptable (yet hard to predict) state of the system.
Because of this conceptual difference, 
we do not have a clear perspective as to how 
known models of exceptions/compensations can be used to 
express the adaptation capabilities that 
are expressible in
our %session-typed 
framework. % is able to represent.

%\todo{
In contrast, more related to our approach is the recent work~\cite{DBLP:conf/aplas/AndersonR12}, 
where dynamic runtime update for message passing programs with queues is studied, 
and 
a form of consistency for updates over threads is ensured using 
multiparty session types.
As in our setting,
the notion of update in~\cite{DBLP:conf/aplas/AndersonR12} does not require
  a complete system shutdown, while ensuring that the state of the program remains consistent. There are significant 
  conceptual and technical differences between our work and~\cite{DBLP:conf/aplas/AndersonR12}. 
First, unlike our approach, in~\cite{DBLP:conf/aplas/AndersonR12} update actions (or adaptation routines)
are defined independently and externally from the program's syntax. 
Second,  here we have considered synchronous communication, 
whereas in~\cite{DBLP:conf/aplas/AndersonR12} an asynchronous thread model with queues is used.
Third, while we have analyzed updates for a language endowed with  binary session types, 
in~\cite{DBLP:conf/aplas/AndersonR12} the need for reaching agreements on multiple threads leads to the use of multiparty session 
types to ensure consistent updates.
It is instructive to note that approaches similar to ours can also be found in the sequential formalisms for reasoning at lower levels of abstraction. For instance, in \cite{DBLP:journals/toplas/StoyleHBSN07} the authors introduce dynamic updates to C-like languages, with a focus on runtime update of functions and type declarations. 
They show that dynamic updates are type-safe (consistent) as it cannot happen that different parts of the program expect
different representations of a type. Although the aim is similar, 
it is difficult to establish more precise comparisons, for our interest is in high-level reasoning for communicating programs with precise protocol descriptions.
%clearly, the setting is completely different as moving from a sequential to a concurrent scenario changes considerably the techniques and the problems to be solved.
%}
 In~\cite{DBLP:conf/amast/BrogiCP04} the authors also investigate behavioral types for adaptation, but 
 in the different setting of component-based systems.
Their notion of runtime adaptation %  \todo{different how?} 
relies on a notion of interface which describes the 
behavior of each component. These interfaces are to be used to implement inter-component communication. 
As it could that composition might not work because of  interface mismatching, 
the authors introduce the notion of  \emph{adaptors}, i.e., a software piece that  acts as mediator between two communicating components. It is interesting to notice that a similar mediator behavior could be implemented in our setting, as described in Sect. \ref{ss:behdist}.
%}



As already discussed, % along the paper, 
our approach has been influenced by~\cite{DBLP:conf/ppdp/GarraldaCD06} and our previous work~\cite{BGPZFMOODS}. 
Nevertheless, 
there are several major differences between 
our framework and those works. %~\cite{DBLP:conf/ppdp/GarraldaCD06}.
(1)~Unlike the system in~\cite{DBLP:conf/ppdp/GarraldaCD06}, our framework supports channel passing (delegation).
As delegation is already useful to 
represent forms of dynamic reconfiguration, its interplay with update actions is very appealing (cf. the example in Sect.~\ref{ss:behdist}).
%\jp{this is no longer useful} 
(2)~We have extended typing
judgments in~\cite{DBLP:conf/ppdp/GarraldaCD06} with \emph{interfaces} $\INT$, which are % of processes.
central to characterize located processes which can be safely updated. 
%with its two zones, $\Delta_l$ and $\Delta_u$. % and by the necessity of distinguishing between linear and unrestricted actions.
%Another distinctive feature of our approach is the treatment in the typing of the restriction operator. 
%In our setting, communication can happen at any level in the hierarchy of adaptable processes; hence, 
%in order to correctly type the number of active sessions (which, as discussed, is central to enable evolvability steps), the information on used session (e.g. $c:\bot$) cannot be hidden.
%Differences with respect to our previous work~\cite{BGPZFMOODS} are also important.
(3)~While in~\cite{BGPZFMOODS} adaptable processes are defined for a %(restriction-free) 
fragment of CCS, 
here we consider them within a typed $\pi$-calculus.
(4)~Adaptation steps in~\cite{BGPZFMOODS} are completely unrestricted. 
%i.e., an update will occur as soon as a located process and an update prefix are able to interact. 
Here we have considered annotated versions of the constructs in~\cite{BGPZFMOODS}:
% Here we have added two elements 
%which serve as a guard for enabling evolvability steps: the number of open sessions in the located processes
%and the interface $\Delta$, present both in the located process and in interacting update processes.
%we think that %our framework enhances the main insights of~\cite{BGPZFMOODS} by 
%they allow to represent evolvable, concurrent systems in a more realistic way, as
%taking the idea of adaptable process to a much more realistic setting, in which 
they offer a more realistic account of update actions, as they are supported 
by runtime conditions based on session types. %d, structured behavior. %determined by the runtime behavior of the system.





%\jp{Other related stuff: \cite{DBLP:conf/aplas/AndersonR12}, possibly also related: \cite{DBLP:conf/isola/LaneseM10,Ivan-Adaptive_C:2013}}
\section{Concluding Remarks}\label{sec:conc}
In this paper we have proposed a  framework for
%alternative \todo{approach?} for 
%specifying and 
reasoning about \emph{runtime ad\-ap\-ta\-tion} in the context of structured communications
described by session types.
Amalgamating a static analysis technique for correct communications (session types) 
with a novel, inherently dynamic form of interaction (as defined by update actions on located processes) is challenging, for 
it requires balancing two different (but equally important) concerns in modern interacting systems. 
In our approach, we investigated a session types discipline for an
extended $\pi$-calculus, in which channel mobility (delegation) is enhanced 
with the possibility of performing sophisticated update actions on located processes.
We purposefully aimed at integrating existing, well-studied lines of work: we expect this to be beneficial  for the 
enhancement of other known session types disciplines with adaptation concerns. 
In particular, we built upon our previous work on  
abstractions for evolvability in process calculi~\cite{BGPZFMOODS} and
on session types for mobile calculi~\cite{DBLP:conf/ppdp/GarraldaCD06}, relying also on 
a modern account of binary session types~\cite{DBLP:journals/entcs/YoshidaV07}.
In addition to runtime correctness (safety), our typing discipline
ensures consistency: this guarantees that communication behavior (as declared by types) is not disrupted by potential update actions.

%It is aimed at supporting the analysis of service-oriented applications/systems.





A main motivation for our work is the observation that while 
paradigms such as service-oriented computing are increasingly popular among practitioners, % software architects and programmers,
formal  models  based on them---such
%core programming calculi based on them---such
as reasoning techniques based on session types---fail to capture  
distinctive aspects of such par\-a\-digms.
Here we have aimed at addressing, for the first time, one of such aspects, namely runtime adaptation. 
In our view, it
%Here we have addressed one such aspects, runtime adaptation, 
represents an increasingly important concern when analyzing the behavior of communicating systems in 
%, which is intimately related to the fact that service oriented systemsare increasingly being deployed in very highly 
open, context-aware computing infrastructures.
%Our proposal, we believe, combines the most interesting aspects of these previous works in the context of the unexplored setting of evolvable session-typed processes. 
%\newpage
%
%As future work, we plan to investigate stronger notions of correctness for our adaptable, session-typed processes, in particular deadlock-freedom.
%Also, following~\cite{DBLP:journals/acta/GayH05} and the discussion in Sect.\ref{sec:int}, 
%we would like to integrate subtyping into our type system,
%and to obtain algorithmic characterizations
%of notions such as type duality and interface compatibility. 
%This work is an initial 
%step towards a theory of interaction
%in which processes---endowed with behavioral disciplines expressed as types---may dynamically evolve at runtime. 
In future work, we plan to investigate 
the interplay of adaptation with
issues such as subtyping, deadlock-freedom, resource usage, and trustworthiness, %, and reliability 
which are also important and challenging. %---we plan to look into these in the future. 
Nevertheless, we believe 
our work already contributes to the understanding of 
%that a major contribution of our paper %is novel, as it  is to address 
issues which, to our knowledge, have not yet  been explored in the realm of 
session-typed %interacting 
processes. 

% . \\%ways of enabling evolvability steps. \\
%-As future work, we plan to investigate stronger notions of correctness for adaptable, session-typed processes, and 
%to develop a formal treatment of subtyping and interface compatibility, along the discussion in Sect.\ref{sec:int}. \\%ways of enabling evolvability steps. \\



\paragraph{Acknowledgments}
%We thank 
%Ant\'{o}nio Ravara,
%Fabrizio Montesi, 
% and
%the SAC'13 and PLACES'13 
%anonymous reviewers for their useful and detailed remarks. 
This work was 
partially 
supported by the French projects 
ANR-11-INSE-0007- REVER and
ANR BLAN 0307 01 - SYNBIOTIC, as well as 
by the 
%Funda\c{c}\~{a}o para a Ci\^{e}ncia e a Tecnologia (
Portuguese Foundation for Science and Technology (FCT) %) 
through the Carnegie Mellon Portugal Program (grant
INTERFACES NGN-44 / 2009)
and grants  CITI and
SFRH\;/\;BPD\;/\;84067\;/\;2012.
 
%We thank the anonymous reviewers for their useful comments.


